/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.Iterator;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.Expr;
import alloy.ast.Id;
import alloy.ast.Multiplicity;
import alloy.ast.Node;
import alloy.ast.Qualifiers;
import alloy.ast.QuantifiedExpr;
import alloy.ast.SetMultExpr;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.UnionType;

/**
 * <p>desugars the relational override visitor as follows:<br>
 * if r1 and r2 have type T1 -> T2 -> ... -> Tn,<br>
 * then r1 ++ r2 = r2 + (r1 & ( (T1 - { t1 : T1 | some t1.r2 }) -> T2 -> ... -> Tn ))
 *
 * if r1 has the type A1 -> A2 -> ... -> Bn + B1 -> B2 -> ... -> Bn and r2 has the
 * type C1 -> C2 -> ... -> Cn + D1 -> D2 -> ... -> Dn then
 * r1 ++ r2 = r2 + (r1 & ( (A1 - { a1 : A1 | some a1.r2}) -> A2 -> ... -> An +
 *                         (B1 - { b1 : B1 | some b1.r2}) -> B2 -> ... -> Bn))  

*/

public class DesugarOverrideVisitor extends ASTDepthFirstReplacer {

    public Object visit(BinaryExpr binExpr_) {
        Expr ret = binExpr_;
        if (binExpr_.getOp().equals(BinaryExprOp.RELATIONALOVERRIDE)) {
            Expr left = (Expr) binExpr_.getLeft().applyReturnVisitor(this);
            Expr right = (Expr) binExpr_.getRight().applyReturnVisitor(this);
            UnionType uType = left.getType();
            BinaryExpr replacement;
	    //System.out.println("in desugar++: " + binExpr_.nodeString());
            // check for easy case of arity 1
            if (uType.arity() == 1) {
                replacement = left.union(right);
            } else {
		// we construct the expression (T1 - { t1 : T1 | some t1.r2}) -> T2 -> ... -> Tn
		// for each RelationType T1 -> T2 -> ... -> Tn in uType and sum them all together
		// to get the expression ( (A1 - { a1 : A1 | some a1.r2}) -> A2 -> ... -> An +
		// (B1 - { b1 : B1 | some b1.r2}) -> B2 -> ... -> Bn) in the example
		BinaryExpr sumExpr = null;
		Iterator relTypeIter = uType.getTypeIter();
		while (relTypeIter.hasNext()) {
		    RelationType relType = (RelationType) relTypeIter.next();
		    
		    // get the domain type of the current relation type & the corresponding expression
		    BasicType domainType = relType.getBasicTypeAt(0);
		    Expr domainExpr = domainType.toExpr();
		    
		    // construct expressions for the range of the current relation type
		    // (i.e. T2-> ... -> Tn)
		    Expr rangeExpr = null;
		    for (int i = 1; i < relType.numBasicTypes(); i++) {
			if (rangeExpr == null) {
			    rangeExpr = relType.getBasicTypeAt(i).toExpr();
			} else {
			    rangeExpr = rangeExpr.product(relType.getBasicTypeAt(i).toExpr());
			}
		    }
		    Expr modifiedDomainExpr = ((Expr)domainExpr.copy());
		    // check that a join between t1 and r2 is possible; if not, just add the
		    // entire product representing the current relation type to the sum
		    if (!right.getType().domainRestrict(domainExpr.getType()).isEmpty()) {		    
			// t1.r2 
			Id id = Id.generateId(domainType.toString());
			VariableExpr varExpr = new VariableExpr(new Variable((Id) id.copy()));
			varExpr.setType(new UnionType(new RelationType(domainType)));
			BinaryExpr binExpr1 = varExpr.join((Expr)right.copy());
			
			// some t1.r2
			QuantifiedExpr quantExpr = QuantifiedExpr.some(binExpr1);

			// t1: T1
			Variables vars = new Variables();
			vars.addVariable(new Variable((Id) id.copy()));
			Decls decls = new Decls();
			SetMultExpr multExpr =
			    new SetMultExpr(Multiplicity.NONE, (Expr) domainExpr.copy());
			multExpr.setType(new UnionType(new RelationType(domainType)));
			decls.addDecl(
				      new Decl(
					       new Qualifiers(),
					       vars,
					       multExpr));
			
			// { t1 : T1 | some t1.r2 }
			ComprehensionExpr compExpr = new ComprehensionExpr(decls, quantExpr, true);
			compExpr.setType(new UnionType(new RelationType(domainType)));
			// T1 - { t1 : T1 | some t1.r2 }
			modifiedDomainExpr = modifiedDomainExpr.diff(compExpr);
		    }

		    modifiedDomainExpr.setType(domainExpr.getType());
		    // (T1 - { t1 : T1 | some t1.r2 }) -> T2 -> ... -> Tn or
		    // T1 -> T2 -> ... -> Tn if t1.r2 is not possible
		    BinaryExpr binExpr3 = modifiedDomainExpr.product((Expr)rangeExpr.copy());
		    
		    // now we add binExpr3 to sumExpr
		    if (sumExpr == null)
			sumExpr = binExpr3;
		    else
			sumExpr = sumExpr.union(binExpr3);
		}
		
		// r1 & ( (A1 - { a1 : A1 | some a1.r2}) -> A2 -> ... -> An +
		//        (B1 - { b1 : B1 | some b1.r2}) -> B2 -> ... -> Bn)
		BinaryExpr binExpr4 = ((Expr)left.copy()).intersect(sumExpr);
		// r2 + (r1 & ( (A1 - { a1 : A1 | some a1.r2}) -> A2 -> ... -> An +
		//              (B1 - { b1 : B1 | some b1.r2}) -> B2 -> ... -> Bn))
		replacement = ((Expr)right.copy()).union(binExpr4);
            }
            replacement.annotateTransformReplacing("desugaring of override", binExpr_);
            ret = replacement;

        } else {
            // if the opcode isn't relational override, desugar the children
            return super.visit((Node)binExpr_);
        }
	//System.out.println("Desugared " + binExpr_.nodeString());
	//System.out.println("to " + ret.nodeString());
        return ret;
    }
}

